Inductive predicates.md (1400B)
1 +++ 2 title = 'Inductive predicates' 3 +++ 4 # Inductive predicates 5 This is basically "logic programming." 6 Inductive predicates: inductively defined propositions, way to specify functions of type `... → Prop`. 7 8 Example for even numbers: 9 10 ```lean 11 inductive even : Ν → Prop 12 | zero : even 0 13 | add_two : ∀k : Ν, even k → even (k+2) 14 ``` 15 16 To check if a list is sorted: 17 18 ```lean 19 inductive sorted : list Ν → Prop 20 | nil : sorted [] 21 | single {x : Ν} : sorted [x] 22 | two_or_more {x y : Ν} {zs : list Ν} (hle : x ≤ y) (hsorted : sorted (y :: zs)) : 23 sorted (x :: y :: zs) 24 ``` 25 26 You can use this to specify 'states'. 27 28 Logical symbols are specified like this: 29 30 ```lean 31 inductive and (a b : Prop) : Prop 32 | intro : a → b → and 33 34 inductive or (a b : Prop) : Prop 35 | intro_left : a → or 36 | intro_right : b → or 37 ``` 38 39 Rule induction: induction in a proof term. The induction is on the introduction rules (constructors of proof term). 40 41 For example: 42 43 ```lean 44 lemma mod_two_eq_zero_of_even (n : Ν) (h : even n) : 45 n % 2 = 0 := 46 begin 47 induction' h, 48 case zero { refl }, 49 case add_two : k hk ih { simp [ih] } 50 end 51 ``` 52 53 Other way to eliminate: 54 * `cases'`: like `induction'`, but without induction hypothesis 55 * `match` corresponds to dependently typed pattern matching 56 57 It's convenient to use the `inversion rule`: `∀x y, p (c x y ) → (∃..., ... ∧ ...) ∨ ... ∨ (∃..., ... ∧ ...)` 58